Nuprl Lemma : l_member-permute
11,40
postcript
pdf
T
:Type,
as
,
bs
:(
T
List),
x
:
T
. (
x
as
@
bs
)
(
x
bs
@
as
)
latex
Definitions
(
x
l
)
,
P
Q
,
Type
,
left
+
right
,
type
List
,
s
=
t
,
a
<
b
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
{
T
}
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
x
.
t
(
x
)
Lemmas
iff
wf
,
all
functionality
wrt
iff
,
iff
functionality
wrt
iff
,
member
append
,
l
member
wf
origin
T:Type, as, bs:(T List), x:T. (x 
as @ bs) 
(x bs @ as) T:Type, as, bs:(T List), x:T. (x as @ bs) (x bs @ as) l)
Q
B(x)
x:A. B(x)
B(x)x:A. B(x) Q Q Q
x. t(x)